package interfaces.gestores;

import interfaces.IProducto;
import tdg.contract.semanticAnnotations.ImportClass;
import tdg.contract.semanticAnnotations.Init;
import tdg.contract.semanticAnnotations.Pre;
import tdg.contract.semanticAnnotations.Pos;
import tdg.contract.semanticAnnotations.Inv;
import tdg.contract.semanticAnnotations.Query;

@Init ({""})
@Inv ({""})

public interface IGestorProductos {
	
	@Pre ({"p!=null #NullPointerException"})
	public void altaProducto(IProducto p);
	
	@Pre ({"p!=null #NullPointerException"})
	public void bajaProducto(IProducto p);
	
	@Pre ({"p1!=null && p2!=null #NullPointerException", "p1.getCodigo()==p2.getCodigo()"})
	public void modificacionProducto(IProducto p1, IProducto p2);
}
